| Definitions | Id, Type, Void, f(x)?z, Knd, lnk-decl(l;dt), KindDeq, f  g, rcv(l,tg), t  T,  x:A. B(x),  x:A.B(x), Top, Valtype(da;k), x : v, State(ds), x:A  B(x), IdDeq,  x.A(x),  x. t(x), S  T, State(ds), f(a), DeclaredType(ds;x), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi ,  b,  A,  b, s = t,  ,  , x dom(f), P   Q, x:A  B(x), P & Q, P  Q, Unit, left + right, a:A fp B(a), Rrframe(loc;x;L), R-Feasible(R), only members of L read x, Rbframe(loc;k;L), k sends only on links in L, Raframe(loc;k;L), k affects only members of L, Rpre(loc;ds;a;p;P), suptype(S; T), (precondition a:Outcome(p) is P:State(ds) -> Bool), Rsends(ds;knd;T;l;dt;g), type List, with declarations ds:dsda:dak(v) sends f s v on link l, Reffect(loc;ds;knd;T;x;f),  , with declarations ds:dsda:daeffect of k(v) is x := f s v, Rsframe(lnk;tag;L), only L sends on (l with tg), Rframe(loc;T;x;L), only members of L affect x :t, Rinit(loc;T;x;v), x : t initially x = v, left right, , Rnone(), es realizer ind Rrframe compseq tag def, es realizer ind Rbframe compseq tag def, es realizer ind Raframe compseq tag def, es realizer ind Rpre compseq tag def, es realizer ind Rsends compseq tag def, es realizer ind Reffect compseq tag def, es realizer ind Rsframe compseq tag def, es realizer ind Rframe compseq tag def, es realizer ind Rinit compseq tag def, es realizer ind Rplus compseq tag def, es realizer ind Rnone compseq tag def, R-base-ma(R), IdLnk, FinProbSpace, rec(x.A(x)), Realizer, MsgA, P Q, <a, b>, True, lnk(k), tag(k), isrcv(k),  T, {T}, SQType(T), s ~ t |